Enum isotope::term::Term[][src]

pub enum Term {
Show variants App(App), Lambda(Lambda), Pi(Pi), Var(Var), Universe(UniverseTerm), Refl(Refl), Id(Id), Enum(Enum), Variant(Variant), Boolean(Boolean), Bool(Bool), Case(Case), Dynamic(DynamicTerm),
}
Expand description

An enumeration of terms in isotope’s term language

Variants

App(App)

A function application

Lambda(Lambda)

A lambda function

Pi(Pi)

A dependent function type

Var(Var)

A variable

Universe(UniverseTerm)

A typing universe

Refl(Refl)

The reflexivity axiom

Id(Id)

Identity types

Enum(Enum)

An enumeration

Variant(Variant)

A variant of an enumeration

Boolean(Boolean)

A boolean term

Bool(Bool)

The type of booleans

Case(Case)

A case statement

Dynamic(DynamicTerm)

A dynamic term

Implementations

Convert a term to it’s prettyprinted string

Convert a term to it’s prettyprinted string for debugging

Trait Implementations

Immutably borrows from an owned value. Read more

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

The type this conses to

Cons this term within a given context. Return None if already consed.

Convert this term to it’s own consed type

Get this term, but consed

Formats the value using the given formatter. Read more

Performs the conversion.

Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class

Get the variable filter of this term

Get the free variable bound of this term

Get whether a term depends on a variable base <= variable <= ix Read more

Feeds this value into the given Hasher. Read more

Feeds a slice of this type into the given Hasher. Read more

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

The type this substitutes to

Substitute this value recursively

Convert this object’s consed form to it’s substituted form

Shift this term’s variables with index >= base in a given context

Shift this term’s variables with index >= base in a given context

Substitute this term’s variables with index >= base down a variable in a given context

Compare this value to another within a given context

Recursively convert this term to an AST in a given context, without it’s annotation

Locally typecheck a term: note this is context-independent, without caching

Globally typecheck a term, i.e. typecheck all subterms, without caching

Typecheck this term’s annotation, without caching

Typecheck a term in a given context

Load this term’s current flags

Set this term’s flags. May cause errors if done incorrectly!

Locally typecheck a term: note this is context-independent.

Globally typecheck a term, i.e. typecheck all subterms and their variables

Variable typecheck a term, i.e. typecheck all subterms and their variables.

Typecheck this term’s annotation

Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables

Typecheck this term along with it’s variables

Whether this term might be type-checked

The type of value this is consed to

The type of value this is substituted to

Convert this term to a Term, without any consing

Get the type annotation of this term

Get the index of this term in a program graph. Return None if this term is unindexed

Get whether this term is a type

Get whether this term is a universe

Get whether this term is a function

Get whether this term is a dependent function type

Get whether this term is in “root form”

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Coerce this term to another type, with type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Convert this term to an annotation, with only rudimentary type-checking

Get whether this term is a constant.

Get whether this term is a subtype of another in a given context

Cast this type into another in a given typing context

Get whether this term has a universe in all contexts

Get the hash-code of this term Read more

Get the hash-code of this term if it was untyped Read more

Substitute this term’s variables recursively given a context

Substitute this term’s variables given a context

Shift this term’s variables with index >= base up by n in a given context

Compare this term to another within a given context

Compare this term to a term ID, within a given context

Cons this term within a given context. Return None if already consed.

Convert this term to a TermId within a given context

Apply this value, as a function, to a given vector of arguments in a given context Returns None if there is no change. Pops off consumed arguments. Read more

Apply this value, as a dependent function type, to a given vector of arguments in a given context Returns None if there is no change. Pops off consumed arguments. Read more

Convert this term to a TermId, without any consing

Clone this term to a TermId, without any consing

Clone this term to a TermId within a given context

Clone this term to a Term without any consing

Get the form of this term

Get whether this term is a subtype of another in general

Get whether this term has a pi type in all contexts

Shift this term’s variables with index >= base up by n in a given context

Get the type of this term, if any

Get the type of this term, if any

Get the transported type of this term, if any

Get the base type of this term, if any

Get the type of this term, if any

Shallow cons a term directly into a context

Shallow cons a term directly into a context, cloning if necessary

Get whether this term is in head normal form

Get whether this term is in beta normal form

Get whether this term is in eta normal form

Convert this term to a normal form

Convert this term a normal form

Convert this term to a normal form, or reduce it up to n steps

Convert this term a normal form, or reduce it up to n steps

Convert this term to a normal form, or reduce it up to n steps

Convert this term a normal form, or reduce it up to n steps

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Borrow an optional value of type T

Hash this using a given hasher

Cons this term within a given context. Return None if already consed.

Get the type annotation of this term

Get the index of this term in an isotope program graph, if any

Get the hash-code of this term

Get whether this term is a type

Get whether this term is a universe

Get whether this term is in “root form”

Get whether this term is a subtype of another term in a given context

Get whether this term has a universe in all contexts

Get the untyped hash-code of this term

Get the variable filter of this term

Shift this term’s variables with index >= base up by n in a given context

Whether this term has a given variable dependency

Whether this term has a given variable dependency below ix and above base

Load this term’s flags

Set this term’s flags

Compare this term to another dynamic term

Convert this term to an Any

Compare this term to another

Compare this term to a term ID

Compare self to key and return true if they are equal.

Performs the conversion.

Performs the conversion.

The resulting type after obtaining ownership.

Creates owned data from borrowed data, usually by cloning. Read more

🔬 This is a nightly-only experimental API. (toowned_clone_into)

recently added

Uses borrowed data to replace owned data, usually by cloning. Read more

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.